$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), ${\it es}$:ES, $x$, $i$:Id, $v$:$T$.
\\[0ex]@$i$ $x$ initially $v$:$T$ $\Rightarrow$ $\forall$$e$@$i$. (($x$ when $e$) = $v$) $\vee$ (lastchange($x$;$e$) $<$ $e$)